A:Type, B:(AType), f:a:A fp B(a), eq:EqDecider(A).   f ~ <1of(f),a.2of(f)(a)> 

latex

Definitions	EqDecider(T), x. t(x), x(s), f(a), Type, a:A fp B(a), x:AB(x), , f  g, f(x)?z, x  dom(f), f(x), S  T, x:A. B(x), x:AB(x), type List, Top, x:A. B(x), t  T, Void
Lemmas	top wf, filter tt, fpf wf, deq wf